atoms-distinct(tab) == i, j:||tab|| . st-atom(tab;i) = st-atom(tab;j)  i = j 

latex

---

clarification:

atoms-distinct(tab)
== i:{0..||tab|| }, j:{0..||tab|| }. st-atom(tab;i) = st-atom(tab;j)  Atom1  i = j   

latex

Definitions	x:A. B(x), {i..j}, #$n, ||tab|| , P  Q, Atom$n, st-atom(tab;n), s = t,
FDL editor aliases	st-atoms-distinct